M1, M2:MsgA, k:Knd. M1  M2  M2.da(k)  M1.da(k) 

latex

Definitions	M.da(a), M1  M2, MsgA, Valtype(da;k), A & B, P & Q, x:A. B(x), P  Q, Top, Knd, KindDeq, t  T
Lemmas	Kind-deq wf, Knd wf, top wf, subtype-fpf-cap-top, msga wf, ma-sub wf